/*
   Copyright (c) 2011, 2012 Mizar Tools Contributors (mizartools.org)

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*/
/*  Contributors :
 *	2011-02-18 Marco Riccardi - initial implementation
 *  2012-04-06 Marco Riccardi - added message in DliParseException
 *
 */
package org.mizartools.dli;

public class Scheme extends ItemDefinition {

	private String name = null;
	private Parameters parameters = null;
	private Premisses premisses = null;
	private Thesis thesis = null;
	
	private Scheme(){
		super(null);
	}

	public Scheme(String name, Parameters parameters, Premisses premisses, Thesis thesis){
		super(null);
		this.name = name;
		this.parameters = parameters;
		this.premisses = premisses;
		this.thesis = thesis;
	}
	
	public static ItemDefinition newInstance(String string) throws DliParseException {
		Scheme predicateNotation = new Scheme();
		int position = string.indexOf("(");
		if (position == -1) {
			throw new DliParseException("["+string+"] is not valid in Scheme");
		}
		if (!string.substring(0, position).equals("scheme")) {
			throw new DliParseException("["+string+"] is not valid in Scheme");
		}
		string = string.substring(position+1, string.length()-1);
		int positionComma = Utility.searchSeparationComma(string);
		if (positionComma == -1) {
			throw new DliParseException("["+string+"] is not valid in Scheme");
		}
		predicateNotation.name = string.substring(0, positionComma);
		string = string.substring(positionComma+1, string.length());
		positionComma = Utility.searchSeparationComma(string);
		String type = null;
		while (positionComma != -1) {
			position = string.indexOf("(");
			int positionCommaTest = string.indexOf(",");
			if (positionCommaTest != 0 && positionComma<position){
				position = positionCommaTest;
			}
			if (position == -1) {
				throw new DliParseException("["+string+"] is not valid in Scheme");
			}
			type = string.substring(0, position);
			if (type.equals("$parameters")){
				predicateNotation.parameters = Parameters.newInstance(string.substring(0, positionComma));
			} else if (type.equals("$premisses")){
				predicateNotation.premisses = Premisses.newInstance(string.substring(0, positionComma));
			} else if (type.equals("$thesis")){
				predicateNotation.thesis = Thesis.newInstance(string.substring(0, positionComma));
			} else {
				throw new DliParseException("["+string+"] is not valid in Scheme");
			}
			string = string.substring(positionComma+1, string.length());
			positionComma = Utility.searchSeparationComma(string);
		}
		position = string.indexOf("(");
		if (position == -1) {
			throw new DliParseException("["+string+"] is not valid in Scheme");
		}
		type = string.substring(0, position);
		if (type.equals("$parameters")){
			predicateNotation.parameters = Parameters.newInstance(string);
		} else if (type.equals("$premisses")){
			predicateNotation.premisses = Premisses.newInstance(string);
		} else if (type.equals("$thesis")){
			predicateNotation.thesis = Thesis.newInstance(string);
		} else {
			throw new DliParseException("["+string+"] is not valid in Scheme");
		}
		return predicateNotation;
	}

	@Override
	public String toString() {
		StringBuilder sb = new StringBuilder();
		sb.append("scheme(");
		if (name != null){
			sb.append(name.toString());
		}
		if (parameters != null){
			sb.append(",");
			sb.append(parameters.toString());
		}
		if (premisses != null){
			sb.append(",");
			sb.append(premisses.toString());
		}
		if (thesis != null){
			sb.append(",");
			sb.append(thesis.toString());
		}
		sb.append(")");
		return sb.toString();
		
	}

	public String getName() {
		return name;
	}

	public Parameters getParameters() {
		return parameters;
	}

	public Premisses getPremisses() {
		return premisses;
	}

	public Thesis getThesis() {
		return thesis;
	}
	
}
